\begin{tabbing}
ma{-}frame{-}compat($A$;$B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=IdIdDeq$\forall$$a$$\in$dom(($A$.2.2.2).1). $p$=($A$.2.2.2).1($a$) $\Rightarrow$  $B$.rframe($A$.pre $p$ for $a$)\+
\\[0ex]\& (:Knd $\times$ Id)product{-}deq(Knd;Id;KindDeq;IdDeq)$\forall$${\it kx}$$\in$dom(($A$.2.2.2.2).1). 
\\[0ex]
\\[0ex]${\it ef}$\==($A$.2.2.2.2).1(${\it kx}$) $\Rightarrow$ \+
\\[0ex]$B$.frame(${\it kx}$.1 affects ${\it kx}$.2)
\-\\[0ex]\& $B$.aframe(${\it kx}$.1 affects ${\it kx}$.2)
\\[0ex]\& $B$.rframe($A$.effect ${\it ef}$ of ${\it kx}$.1 on ${\it kx}$.2)
\\[0ex]\& \=(:Knd $\times$ IdLnk)product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq)$\forall$${\it kl}$$\in$dom(($A$.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]${\it snd}$\==($A$.2.2.2.2.2).1(${\it kl}$) $\Rightarrow$ \+
\\[0ex]($\forall$${\it tg}$:Id. (${\it tg}$ $\in$ map($\lambda$$p$.$p$.1;${\it snd}$) $\in$ Id) $\Rightarrow$ $B$.sframe(${\it kl}$.1 sends $<$${\it kl}$.2,${\it tg}$$>$))
\-\\[0ex]\& $B$.bframe(${\it kl}$.1 sends on ${\it kl}$.2)
\\[0ex]\& $B$.rframe($A$.sends ${\it snd}$ of ${\it kl}$.1 on ${\it kl}$.2)
\-\-
\end{tabbing}